ePMC

Benchmark
Model:consensus v.1 (MDP)
Parameter(s)N = 6, K = 2
Property:steps_min (exp-reward)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files consensus.6.prism --model-input-type prism --property-input-files consensus.props --property-input-names steps_min --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const K=2
Execution
Walltime:112.37370228767395s
Return code:0
Relative Error:0.00011206921961782408
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property steps_min
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 22162 22162
build-model-states-explored 65871 43708
build-model-states-explored 112340 46469
build-model-states-explored 176667 64328
build-model-states-explored 222565 45898
build-model-states-explored 290342 67776
build-model-states-explored 354978 64637
build-model-states-explored 420135 65156
build-model-states-explored 443191 23057
build-model-states-explored 508629 65438
build-model-states-explored 564111 55482
build-model-states-explored 619393 55282
build-model-states-explored 674735 55342
build-model-states-explored 736136 61401
build-model-states-explored 798641 62505
build-model-states-explored 872138 73496
build-model-states-explored 945773 73635
build-model-states-explored 1000069 54297
build-model-states-explored 1005690 5621
build-model-states-explored 1092771 87080
build-model-states-explored 1179387 86616
build-model-done 1258240 21
iterating
iterating-progress-unbounded 37 0.04127721385265479 1
iterating-progress-unbounded 80 0.016333637620158905 2
iterating-progress-unbounded 123 0.009398841728924195 3
iterating-progress-unbounded 166 0.006316358573635542 4
iterating-progress-unbounded 209 0.004562310055392658 5
iterating-progress-unbounded 252 0.003457163104928972 6
iterating-progress-unbounded 295 0.00269440758773604 7
iterating-progress-unbounded 338 0.0021383816271227487 8
iterating-progress-unbounded 381 0.0017330646087645063 9
iterating-progress-unbounded 424 0.001418953097288079 10
iterating-progress-unbounded 467 0.0011743474040158274 11
iterating-progress-unbounded 510 9.775023394167045E-4 12
iterating-progress-unbounded 553 8.162762975550551E-4 13
iterating-progress-unbounded 596 6.877294548501495E-4 14
iterating-progress-unbounded 639 5.808926490214274E-4 15
iterating-progress-unbounded 682 4.928975314735051E-4 16
iterating-progress-unbounded 725 4.1878937232029133E-4 17
iterating-progress-unbounded 768 3.5576081655362365E-4 18
iterating-progress-unbounded 811 3.039245382851461E-4 19
iterating-progress-unbounded 854 2.597273922529298E-4 20
iterating-progress-unbounded 897 2.225371036154332E-4 21
iterating-progress-unbounded 940 1.9064740786714677E-4 22
iterating-progress-unbounded 983 1.631059129443678E-4 23
iterating-progress-unbounded 1026 1.4015992303964317E-4 24
iterating-progress-unbounded 1069 1.2038126713491229E-4 25
iterating-progress-unbounded 1112 1.0358314699758414E-4 26
iterating-progress-unbounded 1155 8.906484672254218E-5 27
iterating-progress-unbounded 1198 7.644022211848007E-5 28
iterating-progress-unbounded 1240 6.616663382028162E-5 29
iterating-progress-unbounded 1283 5.7074888834299486E-5 30
iterating-progress-unbounded 1326 4.942532591142103E-5 31
iterating-progress-unbounded 1369 4.276068016243848E-5 32
iterating-progress-unbounded 1412 3.702687642737608E-5 33
iterating-progress-unbounded 1455 3.195624687109423E-5 34
iterating-progress-unbounded 1498 2.7639747811314663E-5 35
iterating-progress-unbounded 1541 2.3927370452357724E-5 36
iterating-progress-unbounded 1584 2.0690695440440075E-5 37
iterating-progress-unbounded 1627 1.790888144189911E-5 38
iterating-progress-unbounded 1670 1.54480014052514E-5 39
iterating-progress-unbounded 1714 1.3323641842490131E-5 40
iterating-progress-unbounded 1756 1.155518257201456E-5 41
iterating-progress-unbounded 1799 9.986680476743217E-6 42
iterating-progress-unbounded 1842 8.640049472346613E-6 43
iterating-progress-unbounded 1885 7.448877105105204E-6 44
iterating-progress-unbounded 1928 6.435937012779388E-6 45
iterating-progress-unbounded 1971 5.566575595020875E-6 46
iterating-progress-unbounded 2014 4.808674856588974E-6 47
iterating-progress-unbounded 2057 4.1585850169115135E-6 48
iterating-progress-unbounded 2100 3.583663067529664E-6 49
iterating-progress-unbounded 2143 3.095034571695558E-6 50
iterating-progress-unbounded 2186 2.6760073144266216E-6 51
iterating-progress-unbounded 2229 2.3107771234207807E-6 52
iterating-progress-unbounded 2272 1.9977318510400574E-6 53
iterating-progress-unbounded 2315 1.7209437641303608E-6 54
iterating-progress-unbounded 2358 1.4858069256234695E-6 55
iterating-progress-unbounded 2401 1.2842904756508584E-6 56
iterating-progress-unbounded 2444 1.1086790657720022E-6 57
iterating-progress-unbounded 2487 9.582443483853546E-7 58
iterating-progress-unbounded 2530 8.252584767505278E-7 59
iterating-progress-unbounded 2573 7.123242021717966E-7 60
iterating-progress-unbounded 2616 6.155834472144183E-7 61
iterating-progress-unbounded 2659 5.312920081831478E-7 62
iterating-done 2679 62
model-checking-done 111
command-check-result-is 431.9515860971251 steps_min